COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub[let,jmc]" source
C00005 ENDMK
C⊗;
.require "let.pub[let,jmc]" source;
∂MEM Edward J. McCluskey$John McCarthy$Luckham recommendation$Jan. 2, 1977∞

	Dave Luckham's major recent contribution has been in the area of
applied systems for program verification.  Previously his main activity
was theorem proving, and he has also made contributions to the theory
of computability by various classes of programs.

	I find it difficult to make the precise comparisons you request.
DeBakker, Manna, and Paterson have worked mainly in theoretical areas,
and, in those areas, their contribution has been greater than Luckham's.
Bledsoe works in automatic theorem proving and is still active in that area.
My impression is that Luckham has done better theorem proving than
Loveland, but I don't follow that area closely.  I haven't studied the
work of Lawler.

	My impression is that Luckham's work in applied systems for
program verification is first rank, and I know nothing that would
suggest that anyone else is doing better work.  However, I don't have
a clear picture of who is doing work in the areas.  This is because
my own work in program verification is based on proving facts about
recursively defined functions, and this is a much narrower field than
the sequential programs studied by Luckham and most of the others
in the field.

	Therefore, I must suggest that you put most weight on your
other referees in the field.